$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $n$:$\mathbb{N}^{+}$, $x$:$T$. $f$($f$$^{\mbox{\scriptsize $n$$-$1}}$($x$)) $=$ $f$$^{\mbox{\scriptsize $n$}}$($x$)